A1: dom the adj-map of T = the carrier of T by FUNCT_2:def 1;
A2: Fin the adjectives of T c= bool the adjectives of T by FINSUB_1:13;
BoolePoset the adjectives of T = InclPoset (bool the adjectives of T) by YELLOW_1:4
.= RelStr(# (bool the adjectives of T),(RelIncl (bool the adjectives of T)) #) by YELLOW_1:def 1 ;
then rng the adj-map of T c= the carrier of ((BoolePoset the adjectives of T) opp) by A2;
then reconsider f = the adj-map of T as Function of T,((BoolePoset the adjectives of T) opp) by A1, FUNCT_2:2;
thus ( T is adj-structured implies for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ) :: thesis: ( ( for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ) implies T is adj-structured )

proof

assume the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp) ; :: according to ABCMIZ_0:def 10 :: thesis: for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2)
then reconsider f = the adj-map of T as join-preserving Function of T,((BoolePoset the adjectives of T) opp) ;
let t1, t2 be type of T; :: thesis: adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2)
thus adjs (t1 "\/" t2) = (f . t1) "\/" (f . t2) by WAYBEL_6:2
.= (~ (f . t1)) "/\" (~ (f . t2)) by YELLOW_7:22
.= (adjs t1) /\ (adjs t2) by YELLOW_1:17 ; :: thesis: verum

end;

assume A3: for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ; :: thesis: T is adj-structured

now :: thesis: for t1, t2 being type of T holds f . (t1 "\/" t2) = (f . t1) "\/" (f . t2)

let t1, t2 be type of T; :: thesis: f . (t1 "\/" t2) = (f . t1) "\/" (f . t2)
thus f . (t1 "\/" t2) = adjs (t1 "\/" t2)
.= (adjs t1) /\ (adjs t2) by A3
.= (~ (f . t1)) "/\" (~ (f . t2)) by YELLOW_1:17
.= (f . t1) "\/" (f . t2) by YELLOW_7:22 ; :: thesis: verum

end;

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