let S, T be antisymmetric bounded with_suprema with_infima RelStr ; :: thesis: ( [:S,T:] is complemented implies ( S is complemented & T is complemented ) )
assume A1: for x being Element of [:S,T:] ex y being Element of [:S,T:] st y is_a_complement_of x ; :: according to WAYBEL_1:def 24 :: thesis: ( S is complemented & T is complemented )
A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:] by YELLOW_3:def 2;
thus S is complemented :: thesis: T is complemented

proof

let s be Element of S; :: according to WAYBEL_1:def 24 :: thesis: ex b₁ being M2(the carrier of S) st b₁ is_a_complement_of s
consider t being Element of T;
consider y being Element of [:S,T:] such that
A3: y is_a_complement_of [s,t] by A1;
take y `1 ; :: thesis: y `1 is_a_complement_of s
( [s,t] `1 = s & [s,t] `2 = t & y = [(y `1 ),(y `2 )] ) by A2, MCART_1:7, MCART_1:23;
hence y `1 is_a_complement_of s by A3, Th17; :: thesis: verum

end;

let t be Element of T; :: according to WAYBEL_1:def 24 :: thesis: ex b₁ being M2(the carrier of T) st b₁ is_a_complement_of t
consider s being Element of S;
consider y being Element of [:S,T:] such that
A4: y is_a_complement_of [s,t] by A1;
take y `2 ; :: thesis: y `2 is_a_complement_of t
( [s,t] `1 = s & [s,t] `2 = t & y = [(y `1 ),(y `2 )] ) by A2, MCART_1:7, MCART_1:23;
hence y `2 is_a_complement_of t by A4, Th17; :: thesis: verum