let T1, T2 be non empty TA-structure ; :: thesis: ( TA-structure(# the carrier of T1,the adjectives of T1,the InternalRel of T1,the non-op of T1,the adj-map of T1 #) = TA-structure(# the carrier of T2,the adjectives of T2,the InternalRel of T2,the non-op of T2,the adj-map of T2 #) & T1 is adj-structured implies T2 is adj-structured )
assume A1: TA-structure(# the carrier of T1,the adjectives of T1,the InternalRel of T1,the non-op of T1,the adj-map of T1 #) = TA-structure(# the carrier of T2,the adjectives of T2,the InternalRel of T2,the non-op of T2,the adj-map of T2 #) ; :: thesis: ( not T1 is adj-structured or T2 is adj-structured )
assume the adj-map of T1 is join-preserving Function of T1,((BoolePoset the adjectives of T1) opp ) ; :: according to ABCMIZ_0:def 10 :: thesis: T2 is adj-structured
then reconsider f = the adj-map of T1 as join-preserving Function of T1,((BoolePoset the adjectives of T1) opp ) ;
reconsider g = f as Function of T2,((BoolePoset the adjectives of T2) opp ) by A1;
A2: ( RelStr(# the carrier of T1,the InternalRel of T1 #) = RelStr(# the carrier of T2,the InternalRel of T2 #) & RelStr(# the carrier of ((BoolePoset the adjectives of T1) opp ),the InternalRel of ((BoolePoset the adjectives of T1) opp ) #) = RelStr(# the carrier of ((BoolePoset the adjectives of T2) opp ),the InternalRel of ((BoolePoset the adjectives of T2) opp ) #) ) by A1;
g is join-preserving

proof

let x, y be type of T2; :: according to WAYBEL_0:def 35 :: thesis: g preserves_sup_of {x,y}
reconsider x' = x, y' = y as type of T1 by A1;
assume A3: ex_sup_of {x,y},T2 ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of g .: {x,y},(BoolePoset the adjectives of T2) opp & "\/" (g .: {x,y}),((BoolePoset the adjectives of T2) opp ) = g . ("\/" {x,y},T2) )
then A4: ( ex_sup_of {x',y'},T1 & f preserves_sup_of {x',y'} ) by A2, WAYBEL_0:def 35, YELLOW_0:14;
then A5: ( ex_sup_of f .: {x',y'},(BoolePoset the adjectives of T1) opp & sup (f .: {x',y'}) = f . (sup {x',y'}) ) by WAYBEL_0:def 31;
thus ex_sup_of g .: {x,y},(BoolePoset the adjectives of T2) opp by A1, A4, WAYBEL_0:def 31; :: thesis: "\/" (g .: {x,y}),((BoolePoset the adjectives of T2) opp ) = g . ("\/" {x,y},T2)
thus "\/" (g .: {x,y}),((BoolePoset the adjectives of T2) opp ) = g . ("\/" {x,y},T2) by A2, A3, A5, YELLOW_0:26; :: thesis: verum

end;

hence the adj-map of T2 is join-preserving Function of T2,((BoolePoset the adjectives of T2) opp ) by A1; :: according to ABCMIZ_0:def 10 :: thesis: verum