let S, T be non empty reflexive antisymmetric up-complete RelStr ; for X being upper Subset of S
for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible
let X be upper Subset of S; for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible
let Y be upper Subset of T; ( X is inaccessible & Y is inaccessible implies [:X,Y:] is inaccessible )
assume that
A1:
for D being non empty directed Subset of S st sup D in X holds
D meets X
and
A2:
for D being non empty directed Subset of T st sup D in Y holds
D meets Y
; WAYBEL11:def 1 [:X,Y:] is inaccessible
let D be non empty directed Subset of [:S,T:]; WAYBEL11:def 1 ( not "\/" (D,[:S,T:]) in [:X,Y:] or not D misses [:X,Y:] )
assume A3:
sup D in [:X,Y:]
; not D misses [:X,Y:]
ex_sup_of D,[:S,T:]
by WAYBEL_0:75;
then A4:
sup D = [(sup (proj1 D)),(sup (proj2 D))]
by YELLOW_3:46;
then
( not proj1 D is empty & proj1 D is directed & sup (proj1 D) in X )
by A3, YELLOW_3:21, YELLOW_3:22, ZFMISC_1:87;
then
proj1 D meets X
by A1;
then consider s being object such that
A5:
s in proj1 D
and
A6:
s in X
by XBOOLE_0:3;
reconsider s = s as Element of S by A5;
consider s2 being object such that
A7:
[s,s2] in D
by A5, XTUPLE_0:def 12;
( not proj2 D is empty & proj2 D is directed & sup (proj2 D) in Y )
by A3, A4, YELLOW_3:21, YELLOW_3:22, ZFMISC_1:87;
then
proj2 D meets Y
by A2;
then consider t being object such that
A8:
t in proj2 D
and
A9:
t in Y
by XBOOLE_0:3;
reconsider t = t as Element of T by A8;
consider t1 being object such that
A10:
[t1,t] in D
by A8, XTUPLE_0:def 13;
A11:
the carrier of [:S,T:] = [: the carrier of S, the carrier of T:]
by YELLOW_3:def 2;
then reconsider s2 = s2 as Element of T by A7, ZFMISC_1:87;
reconsider t1 = t1 as Element of S by A11, A10, ZFMISC_1:87;
consider z being Element of [:S,T:] such that
A12:
z in D
and
A13:
[s,s2] <= z
and
A14:
[t1,t] <= z
by A7, A10, WAYBEL_0:def 1;
now ex z being Element of [:S,T:] st
( z in D & z in [:X,Y:] )take z =
z;
( z in D & z in [:X,Y:] )thus
z in D
by A12;
z in [:X,Y:]A15:
z = [(z `1),(z `2)]
by A11, MCART_1:21;
then
t <= z `2
by A14, YELLOW_3:11;
then A16:
z `2 in Y
by A9, WAYBEL_0:def 20;
s <= z `1
by A13, A15, YELLOW_3:11;
then
z `1 in X
by A6, WAYBEL_0:def 20;
hence
z in [:X,Y:]
by A15, A16, ZFMISC_1:87;
verum end;
hence
not D misses [:X,Y:]
by XBOOLE_0:3; verum