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 upper holds
( D1 is upper & D2 is upper )
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds
( D1 is upper & D2 is upper )
let D2 be non empty Subset of S2; :: thesis: ( [:D1,D2:] is upper implies ( D1 is upper & D2 is upper ) )
assume A1: [:D1,D2:] is upper ; :: thesis: ( D1 is upper & D2 is upper )
thus D1 is upper :: thesis: D2 is upper

proof

consider q1 being Element of D2;
let x, y be Element of S1; :: according to WAYBEL_0:def 20 :: thesis: ( not x in D1 or not x <= y 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 20;
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 20 :: thesis: ( not x in D2 or not x <= y 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 20;
hence y in D2 by ZFMISC_1:106; :: thesis: verum