let S1, S2 be non empty reflexive RelStr ; 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; 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; ( [:D1,D2:] is upper implies ( D1 is upper & D2 is upper ) )
assume A1:
[:D1,D2:] is upper
; ( D1 is upper & D2 is upper )
thus
D1 is upper
D2 is upper proof
set q1 = the
Element of
D2;
let x,
y be
Element of
S1;
WAYBEL_0:def 20 ( not x in D1 or not x <= y or y in D1 )
assume that A2:
x in D1
and A3:
x <= y
;
y in D1
A4:
[x, the Element of D2] in [:D1,D2:]
by A2, ZFMISC_1:87;
the
Element of
D2 <= the
Element of
D2
;
then
[x, the Element of D2] <= [y, the Element of D2]
by A3, Th11;
then
[y, the Element of D2] in [:D1,D2:]
by A1, A4;
hence
y in D1
by ZFMISC_1:87;
verum
end;
set q1 = the Element of D1;
let x, y be Element of S2; WAYBEL_0:def 20 ( not x in D2 or not x <= y or y in D2 )
assume that
A5:
x in D2
and
A6:
x <= y
; y in D2
A7:
[ the Element of D1,x] in [:D1,D2:]
by A5, ZFMISC_1:87;
the Element of D1 <= the Element of D1
;
then
[ the Element of D1,x] <= [ the Element of D1,y]
by A6, Th11;
then
[ the Element of D1,y] in [:D1,D2:]
by A1, A7;
hence
y in D2
by ZFMISC_1:87; verum