let T1, T2 be non empty TA-structure ; ( 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 #)
; ( 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 )
; ABCMIZ_0:def 10 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 #)
by A1;
g is join-preserving
proof
let x,
y be
type of
T2;
WAYBEL_0:def 35 g preserves_sup_of {x,y}
reconsider x9 =
x,
y9 =
y as
type of
T1 by A1;
assume A3:
ex_sup_of {x,y},
T2
;
WAYBEL_0:def 31 ( 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 {x9,y9},
T1
by A2, YELLOW_0:14;
A5:
f preserves_sup_of {x9,y9}
by WAYBEL_0:def 35;
hence
ex_sup_of g .: {x,y},
(BoolePoset the adjectives of T2) opp
by A1, A4, WAYBEL_0:def 31;
"\/" (g .: {x,y}),((BoolePoset the adjectives of T2) opp ) = g . ("\/" {x,y},T2)
sup (f .: {x9,y9}) = f . (sup {x9,y9})
by A4, A5, WAYBEL_0:def 31;
hence
"\/" (g .: {x,y}),
((BoolePoset the adjectives of T2) opp ) = g . ("\/" {x,y},T2)
by A1, A2, A3, YELLOW_0:26;
verum
end;
hence
the adj-map of T2 is join-preserving Function of T2,((BoolePoset the adjectives of T2) opp )
by A1; ABCMIZ_0:def 10 verum