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

consider q1 being Element of D2;
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 that
A2: x in D1 and
A3: x >= y ; :: thesis: y in D1
A4: [x,q1] in [:D1,D2:] by A2, ZFMISC_1:106;
q1 <= q1 ;
then [x,q1] >= [y,q1] by A3, Th11;
then [y,q1] in [:D1,D2:] by A1, A4, WAYBEL_0:def 19;
hence y in D1 by ZFMISC_1:106; :: thesis: verum

end;

consider q1 being Element of D1;
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 that
A5: x in D2 and
A6: x >= y ; :: thesis: y in D2
A7: [q1,x] in [:D1,D2:] by A5, ZFMISC_1:106;
q1 <= q1 ;
then [q1,x] >= [q1,y] by A6, Th11;
then [q1,y] in [:D1,D2:] by A1, A7, WAYBEL_0:def 19;
hence y in D2 by ZFMISC_1:106; :: thesis: verum