let T1, T2 be non empty RelStr ; :: thesis: for S1 being non empty full SubRelStr of T1
for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds
S2 is directed-sups-inheriting
let S1 be non empty full SubRelStr of T1; :: thesis: for S2 being non empty full SubRelStr of T2 st RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting holds
S2 is directed-sups-inheriting
let S2 be non empty full SubRelStr of T2; :: thesis: ( RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) & the carrier of S1 = the carrier of S2 & S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting )
assume A1: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; :: thesis: ( not the carrier of S1 = the carrier of S2 or not S1 is directed-sups-inheriting or S2 is directed-sups-inheriting )
RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ;
then reconsider R = S2 as full SubRelStr of T1 by A1, Th12;
assume A2: the carrier of S1 = the carrier of S2 ; :: thesis: ( not S1 is directed-sups-inheriting or S2 is directed-sups-inheriting )
then A3: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_0:57;
assume A4: for X being directed Subset of S1 st X <> {} & ex_sup_of X,T1 holds
"\/" (X,T1) in the carrier of S1 ; :: according to WAYBEL_0:def 4 :: thesis: S2 is directed-sups-inheriting
let X be directed Subset of S2; :: according to WAYBEL_0:def 4 :: thesis: ( X = {} or not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 )
assume A5: X <> {} ; :: thesis: ( not ex_sup_of X,T2 or "\/" (X,T2) in the carrier of S2 )
reconsider Y = X as directed Subset of S1 by A3, WAYBEL_0:3;
assume A6: ex_sup_of X,T2 ; :: thesis: "\/" (X,T2) in the carrier of S2
then "\/" (Y,T1) in the carrier of S1 by A1, A4, A5, YELLOW_0:14;
hence "\/" (X,T2) in the carrier of S2 by A1, A2, A6, YELLOW_0:26; :: thesis: verum