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;
"\/" ((g .: {x,y}),((BoolePoset the adjectives of T2) opp)) = g . ("\/" ({x,y},T2))
sup (f .: {x9,y9}) = f . (sup {x9,y9})
by A4, A5;
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