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