set A = { [s,t] where s is Point of S, t is Point of T : s <> t } ;

{ [s,t] where s is Point of S, t is Point of T : s <> t } c= the carrier of [:S,T:]

{ [s,t] where s is Point of S, t is Point of T : s <> t } c= the carrier of [:S,T:]

proof

hence
{ [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:]
; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [s,t] where s is Point of S, t is Point of T : s <> t } or a in the carrier of [:S,T:] )

assume a in { [s,t] where s is Point of S, t is Point of T : s <> t } ; :: thesis: a in the carrier of [:S,T:]

then ex s being Point of S ex t being Point of T st

( a = [s,t] & s <> t ) ;

hence a in the carrier of [:S,T:] ; :: thesis: verum

end;assume a in { [s,t] where s is Point of S, t is Point of T : s <> t } ; :: thesis: a in the carrier of [:S,T:]

then ex s being Point of S ex t being Point of T st

( a = [s,t] & s <> t ) ;

hence a in the carrier of [:S,T:] ; :: thesis: verum