let S, T be antisymmetric bounded with_suprema with_infima RelStr ; :: thesis: ( [:S,T:] is complemented implies ( S is complemented & T is complemented ) )
set s = the 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
set t = the Element of T;
let s be Element of S; :: according to WAYBEL_1:def 24 :: thesis: ex b1 being M3( the carrier of S) st b1 is_a_complement_of s
consider y being Element of [:S,T:] such that
A2: y is_a_complement_of [s, the Element of T] by A1;
take y `1 ; :: thesis: y `1 is_a_complement_of s
[s, the Element of T] `1 = s ;
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 b1 being M3( the carrier of T) st b1 is_a_complement_of t
consider y being Element of [:S,T:] such that
A3: y is_a_complement_of [ the Element of S,t] by A1;
take y `2 ; :: thesis: y `2 is_a_complement_of t
[ the Element of S,t] `2 = t ;
hence y `2 is_a_complement_of t by A3, Th17; :: thesis: verum