let S1, S2 be non empty reflexive RelStr ; :: thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower & D2 is lower )
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower & D2 is lower )
let D2 be non empty Subset of S2; :: thesis: ( [:D1,D2:] is lower implies ( D1 is lower & D2 is lower ) )
assume A1: [:D1,D2:] is lower ; :: thesis: ( D1 is lower & D2 is lower )
thus D1 is lower :: thesis: D2 is lower

proof

let x, y be Element of S1; :: according to WAYBEL_0:def 19 :: thesis: ( not x in D1 or not y <= x or y in D1 )
assume A2: ( x in D1 & x >= y ) ; :: thesis: y in D1
consider q1 being Element of D2;
A3: [x,q1] in [:D1,D2:] by A2, ZFMISC_1:106;
q1 <= q1 ;
then [x,q1] >= [y,q1] by A2, Th11;
then [y,q1] in [:D1,D2:] by A1, A3, WAYBEL_0:def 19;
hence y in D1 by ZFMISC_1:106; :: thesis: verum

end;

let x, y be Element of S2; :: according to WAYBEL_0:def 19 :: thesis: ( not x in D2 or not y <= x or y in D2 )
assume A4: ( x in D2 & x >= y ) ; :: thesis: y in D2
consider q1 being Element of D1;
A5: [q1,x] in [:D1,D2:] by A4, ZFMISC_1:106;
q1 <= q1 ;
then [q1,x] >= [q1,y] by A4, Th11;
then [q1,y] in [:D1,D2:] by A1, A5, WAYBEL_0:def 19;
hence y in D2 by ZFMISC_1:106; :: thesis: verum