let S, T be antisymmetric bounded with_suprema with_infima RelStr ; :: thesis: ( [:S,T:] is complemented implies ( S is complemented & T is complemented ) )
consider s being Element of S;
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 )
thus S is complemented :: thesis: T is complemented

proof

consider t being Element of T;
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 y being Element of [:S,T:] such that
A2: y is_a_complement_of [s,t] by A1;
take y `1 ; :: thesis: y `1 is_a_complement_of s
[s,t] `1 = s by MCART_1:7;
hence y `1 is_a_complement_of s by A2, 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 y being Element of [:S,T:] such that
A3: y is_a_complement_of [s,t] by A1;
take y `2 ; :: thesis: y `2 is_a_complement_of t
[s,t] `2 = t by MCART_1:7;
hence y `2 is_a_complement_of t by A3, Th17; :: thesis: verum